Notes (Week 4 Monday)

   If some set of numbers A
     (i) contains Z, and
     (ii) contains S n if it contains n,

   then A contains all numbers.


   If some set of numbers A
     (B) Z ∈ A, and
     (I) n ∈ A ⇒ S n ∈ A

   then ∀n∈ℕ. n ∈ A

Q: Is the purpose to ensure the non-existence of
   "external" numbers that have no path to 0
A: Yes: it implies that the numbers obtainable by
   the axioms are the only numbers.

   If we leave out the induction axiom, then we can't
   disprove the existence of a number ω
   s.t.
       ω = S ω


           .. < 1/4 < 1/2 < 1

Q: Does observing that there's no minimal element
   prove that it's not well-founded?
A: Yes!
     R is well-founded
   is equivalent to
     every non-empty subset of R has a
      minimal element

        0 < 1 < 2 < 3

                0  >  -2 > -3


         all the numbers divisibe by 8
          ⊆                                
         all the numbers divisibe by 4
          ⊆
          all the even numbers
          ⊆
          ℕ

          ℕ ⊆ ℕ

z(λ) = λ
z(aw) = 0(z(w))


z(10w) = 0(z(0w))

 ^ the number of 0s in the arguments to z are the
   same on both left and right

open bossLib listTheory rich_listTheory
     arithmeticTheory;

Definition z_def:
  z([]) = [] ∧
  z([a]) = [0] ∧
  z(a::b::w) = 0::z(0::w)
End

Theorem z_zeroizes:
  z w = REPLICATE (LENGTH w) 0
Proof
  Induct_on ‘w’ (* structural induction *)
  >- rw[z_def] >>
  strip_tac >>
  Cases_on ‘w’
  >- rw[z_def,REPLICATE_compute] >>
  rw[z_def] >>
  Cases_on ‘t’ >> gvs[z_def]
QED

Theorem z_zeroizes:
  z w = REPLICATE (LENGTH w) 0
Proof
  Induct_on ‘LENGTH w’ using COMPLETE_INDUCTION >>
  rw[]
  Cases_on ‘w’
  >- rw[z_def] >>
  Cases_on ‘t’ >>
  gvs[z_def,REPLICATE_compute]
QED


⊤⊤∧∧∧∧∧)))))) ∈ Σ*


 a ∧ b ∨ c

 (a ∧ b) ∨ c

 a ∧ (b ∨ c)

 ¬a ∧ b     denotes    ((¬a) ∧ b)

 a ∧ b ∨ c    denotes    ((a ∧ b) ∨ c)


  p → q → r    parses as  p → (q → r)

   which is *different from*

       (p → q) → r


    p → (q → r)   ≡  (p ∧ q) → r

    if p holds,
     then if q holds, r also holds

    if p and q holds, then r holds

In the same way that in posets you can
  instantiate (R,≺) in various ways
  to obtain specific posets

We can instantiate
  T,0,1,∧,∨,'
in various ways to obtain specific boolean
 algebras

In the two-element boolean algebra
  we use &&  (like in C) for conjunction
But in propositional logic formulas
  we use ∧ for conjunction


 &&  computes a truth value

 ∧   builds a bigger formula


 true && true = true (syntactically equals)

 ⊤ ∧ ⊤ ≠ ⊤ (syntactically)

 ^ because the LHS and RHS have different
   parse trees


 𝓟(𝓤) = {{∅},∅}

 if we imagine that false = ∅
   and true = {∅}


   true && false = false


   {∅}  ∩  {}    = {}


Here's the stupidest Boolean algebra:
  the one-element algebra

  ({x},∨,∧,',x,x)

  where   x ∧ x = x
          x ∨ x = x
          x' = x

  all the laws hold in this algebra,
   because in a world where there's only
   one thing, everything is equal.

In this Boolean algebra:

   e'  = e

^ but we can't prove this from the Boolean
  algebra laws only.


  a ∧ b


  ⟦ ⟧  "semantic brackets"


  convention:

    if   φ  is a piece of syntax

    then ⟦φ⟧ reads "the semantics of φ"

  ⟦φ⟧v "the semantics of the formula φ
        under the valuation v"

  These brackets are just fancy notation
  for a function, we could call it "eval"

   instead of writing ⟦φ⟧v
   we could have written
      (say)   eval(φ,v)